$\forall$${\it es}$:ES, $i$:Id, $P$:(state@$i$$\rightarrow$Prop). @$i$ stable ${\it state}$.$P$(${\it state}$)   $\in$ Prop